Left Termination of the query pattern
goal(g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 187 ms)
↳2 TRIPLES
↳3 UndefinedPredicateInTriplesTransformerProof (⇒, 0 ms)
↳4 TRIPLES
↳5 TriplesToPiDPProof (⇒, 21 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
    ↳9 PiDP
        ↳10 UsableRulesProof (⇔, 0 ms)
        ↳11 PiDP
        ↳12 PiDPToQDPProof (⇒, 19 ms)
        ↳13 QDP
        ↳14 QDPSizeChangeProof (⇔, 0 ms)
        ↳15 YES
    ↳16 PiDP
        ↳17 UsableRulesProof (⇔, 0 ms)
        ↳18 PiDP
        ↳19 PiDPToQDPProof (⇒, 0 ms)
        ↳20 QDP
        ↳21 QDPSizeChangeProof (⇔, 0 ms)
        ↳22 YES

(0) Obligation:

Clauses:

goal(X) :- ','(s2l(X, Xs), conf(Xs)).
conf(X) :- ','(del2(X, Z), ','(del(U, Y, Z), conf(Y))).
del2(X, Y) :- ','(del(U, X, Z), del(V, Z, Y)).
del(X1, [], X2) :- ','(!, failure(a)).
del(H, X, T) :- ','(head(X, H), tail(X, T)).
del(X, Y, .(H, T2)) :- ','(head(Y, H), ','(tail(Y, T1), del(X, T1, T2))).
s2l(0, L) :- ','(!, eq(L, [])).
s2l(X, .(X3, Xs)) :- ','(p(X, P), s2l(P, Xs)).
head([], X4).
head(.(H, X5), H).
tail([], []).
tail(.(X6, Xs), Xs).
p(0, 0).
p(s(X), X).
failure(b).
eq(X, X).

Query: goal(g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

delA(X1, [], .(X2, X3)) :- delB(X1, X3).
delA(X1, .(X2, X3), .(X2, X4)) :- delA(X1, X3, X4).
pC(X1, X2, X3) :- ','(delcE(X1, X2, X3), confD(X2)).
confD(X1) :- delA(X2, X1, X3).
confD(X1) :- ','(delcA(X2, X1, X3), delA(X4, X3, X5)).
confD(X1) :- ','(del2cF(X1, X2), pC(X3, X4, X2)).
s2lG(s(X1), .(X2, X3)) :- s2lG(X1, X3).
goalI(0) :- delB(X1, X2).
goalI(0) :- ','(delcB(X1, X2), delA(X3, X2, X4)).
goalI(0) :- ','(del2cH(X1), pC(X2, X3, X1)).
goalI(s(X1)) :- s2lG(X1, X2).
goalI(s(X1)) :- ','(s2lcG(X1, X2), confD(.(X3, X2))).

Clauses:

delcA(X1, [], []).
delcA(X1, .(X1, X2), X2).
delcA(X1, [], .(X2, X3)) :- delcB(X1, X3).
delcA(X1, .(X2, X3), .(X2, X4)) :- delcA(X1, X3, X4).
qcC(X1, X2, X3) :- ','(delcE(X1, X2, X3), confcD(X2)).
confcD(X1) :- ','(del2cF(X1, X2), qcC(X3, X4, X2)).
s2lcG(0, []).
s2lcG(s(X1), .(X2, X3)) :- s2lcG(X1, X3).
del2cH(X1) :- ','(delcB(X2, X3), delcA(X4, X3, X1)).
del2cF(X1, X2) :- ','(delcA(X3, X1, X4), delcA(X5, X4, X2)).

Afs:

goalI(x1)  =  goalI(x1)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [DT09].

(4) Obligation:

Triples:

delA(X1, .(X2, X3), .(X2, X4)) :- delA(X1, X3, X4).
confD(X1) :- delA(X2, X1, X3).
confD(X1) :- ','(delcA(X2, X1, X3), delA(X4, X3, X5)).
s2lG(s(X1), .(X2, X3)) :- s2lG(X1, X3).
goalI(s(X1)) :- s2lG(X1, X2).
goalI(s(X1)) :- ','(s2lcG(X1, X2), confD(.(X3, X2))).

Clauses:

delcA(X1, [], []).
delcA(X1, .(X1, X2), X2).
delcA(X1, .(X2, X3), .(X2, X4)) :- delcA(X1, X3, X4).
s2lcG(0, []).
s2lcG(s(X1), .(X2, X3)) :- s2lcG(X1, X3).
del2cF(X1, X2) :- ','(delcA(X3, X1, X4), delcA(X5, X4, X2)).

Afs:

goalI(x1)  =  goalI(x1)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
goalI_in: (b)
s2lG_in: (b,f)
s2lcG_in: (b,f)
confD_in: (b)
delA_in: (f,b,f)
delcA_in: (f,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

GOALI_IN_G(s(X1)) → U6_G(X1, s2lG_in_ga(X1, X2))
GOALI_IN_G(s(X1)) → S2LG_IN_GA(X1, X2)
S2LG_IN_GA(s(X1), .(X2, X3)) → U5_GA(X1, X2, X3, s2lG_in_ga(X1, X3))
S2LG_IN_GA(s(X1), .(X2, X3)) → S2LG_IN_GA(X1, X3)
GOALI_IN_G(s(X1)) → U7_G(X1, s2lcG_in_ga(X1, X2))
U7_G(X1, s2lcG_out_ga(X1, X2)) → U8_G(X1, confD_in_g(.(X3, X2)))
U7_G(X1, s2lcG_out_ga(X1, X2)) → CONFD_IN_G(.(X3, X2))
CONFD_IN_G(X1) → U2_G(X1, delA_in_aga(X2, X1, X3))
CONFD_IN_G(X1) → DELA_IN_AGA(X2, X1, X3)
DELA_IN_AGA(X1, .(X2, X3), .(X2, X4)) → U1_AGA(X1, X2, X3, X4, delA_in_aga(X1, X3, X4))
DELA_IN_AGA(X1, .(X2, X3), .(X2, X4)) → DELA_IN_AGA(X1, X3, X4)
CONFD_IN_G(X1) → U3_G(X1, delcA_in_aga(X2, X1, X3))
U3_G(X1, delcA_out_aga(X2, X1, X3)) → U4_G(X1, delA_in_aga(X4, X3, X5))
U3_G(X1, delcA_out_aga(X2, X1, X3)) → DELA_IN_AGA(X4, X3, X5)

The TRS R consists of the following rules:

s2lcG_in_ga(0, []) → s2lcG_out_ga(0, [])
s2lcG_in_ga(s(X1), .(X2, X3)) → U11_ga(X1, X2, X3, s2lcG_in_ga(X1, X3))
U11_ga(X1, X2, X3, s2lcG_out_ga(X1, X3)) → s2lcG_out_ga(s(X1), .(X2, X3))
delcA_in_aga(X1, [], []) → delcA_out_aga(X1, [], [])
delcA_in_aga(X1, .(X1, X2), X2) → delcA_out_aga(X1, .(X1, X2), X2)
delcA_in_aga(X1, .(X2, X3), .(X2, X4)) → U10_aga(X1, X2, X3, X4, delcA_in_aga(X1, X3, X4))
U10_aga(X1, X2, X3, X4, delcA_out_aga(X1, X3, X4)) → delcA_out_aga(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
s2lG_in_ga(x1, x2)  =  s2lG_in_ga(x1)
.(x1, x2)  =  .(x2)
s2lcG_in_ga(x1, x2)  =  s2lcG_in_ga(x1)
0  =  0
s2lcG_out_ga(x1, x2)  =  s2lcG_out_ga(x1, x2)
U11_ga(x1, x2, x3, x4)  =  U11_ga(x1, x4)
confD_in_g(x1)  =  confD_in_g(x1)
delA_in_aga(x1, x2, x3)  =  delA_in_aga(x2)
delcA_in_aga(x1, x2, x3)  =  delcA_in_aga(x2)
[]  =  []
delcA_out_aga(x1, x2, x3)  =  delcA_out_aga(x2, x3)
U10_aga(x1, x2, x3, x4, x5)  =  U10_aga(x3, x5)
GOALI_IN_G(x1)  =  GOALI_IN_G(x1)
U6_G(x1, x2)  =  U6_G(x1, x2)
S2LG_IN_GA(x1, x2)  =  S2LG_IN_GA(x1)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x4)
U7_G(x1, x2)  =  U7_G(x1, x2)
U8_G(x1, x2)  =  U8_G(x1, x2)
CONFD_IN_G(x1)  =  CONFD_IN_G(x1)
U2_G(x1, x2)  =  U2_G(x1, x2)
DELA_IN_AGA(x1, x2, x3)  =  DELA_IN_AGA(x2)
U1_AGA(x1, x2, x3, x4, x5)  =  U1_AGA(x3, x5)
U3_G(x1, x2)  =  U3_G(x1, x2)
U4_G(x1, x2)  =  U4_G(x1, x2)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GOALI_IN_G(s(X1)) → U6_G(X1, s2lG_in_ga(X1, X2))
GOALI_IN_G(s(X1)) → S2LG_IN_GA(X1, X2)
S2LG_IN_GA(s(X1), .(X2, X3)) → U5_GA(X1, X2, X3, s2lG_in_ga(X1, X3))
S2LG_IN_GA(s(X1), .(X2, X3)) → S2LG_IN_GA(X1, X3)
GOALI_IN_G(s(X1)) → U7_G(X1, s2lcG_in_ga(X1, X2))
U7_G(X1, s2lcG_out_ga(X1, X2)) → U8_G(X1, confD_in_g(.(X3, X2)))
U7_G(X1, s2lcG_out_ga(X1, X2)) → CONFD_IN_G(.(X3, X2))
CONFD_IN_G(X1) → U2_G(X1, delA_in_aga(X2, X1, X3))
CONFD_IN_G(X1) → DELA_IN_AGA(X2, X1, X3)
DELA_IN_AGA(X1, .(X2, X3), .(X2, X4)) → U1_AGA(X1, X2, X3, X4, delA_in_aga(X1, X3, X4))
DELA_IN_AGA(X1, .(X2, X3), .(X2, X4)) → DELA_IN_AGA(X1, X3, X4)
CONFD_IN_G(X1) → U3_G(X1, delcA_in_aga(X2, X1, X3))
U3_G(X1, delcA_out_aga(X2, X1, X3)) → U4_G(X1, delA_in_aga(X4, X3, X5))
U3_G(X1, delcA_out_aga(X2, X1, X3)) → DELA_IN_AGA(X4, X3, X5)

The TRS R consists of the following rules:

s2lcG_in_ga(0, []) → s2lcG_out_ga(0, [])
s2lcG_in_ga(s(X1), .(X2, X3)) → U11_ga(X1, X2, X3, s2lcG_in_ga(X1, X3))
U11_ga(X1, X2, X3, s2lcG_out_ga(X1, X3)) → s2lcG_out_ga(s(X1), .(X2, X3))
delcA_in_aga(X1, [], []) → delcA_out_aga(X1, [], [])
delcA_in_aga(X1, .(X1, X2), X2) → delcA_out_aga(X1, .(X1, X2), X2)
delcA_in_aga(X1, .(X2, X3), .(X2, X4)) → U10_aga(X1, X2, X3, X4, delcA_in_aga(X1, X3, X4))
U10_aga(X1, X2, X3, X4, delcA_out_aga(X1, X3, X4)) → delcA_out_aga(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
s2lG_in_ga(x1, x2)  =  s2lG_in_ga(x1)
.(x1, x2)  =  .(x2)
s2lcG_in_ga(x1, x2)  =  s2lcG_in_ga(x1)
0  =  0
s2lcG_out_ga(x1, x2)  =  s2lcG_out_ga(x1, x2)
U11_ga(x1, x2, x3, x4)  =  U11_ga(x1, x4)
confD_in_g(x1)  =  confD_in_g(x1)
delA_in_aga(x1, x2, x3)  =  delA_in_aga(x2)
delcA_in_aga(x1, x2, x3)  =  delcA_in_aga(x2)
[]  =  []
delcA_out_aga(x1, x2, x3)  =  delcA_out_aga(x2, x3)
U10_aga(x1, x2, x3, x4, x5)  =  U10_aga(x3, x5)
GOALI_IN_G(x1)  =  GOALI_IN_G(x1)
U6_G(x1, x2)  =  U6_G(x1, x2)
S2LG_IN_GA(x1, x2)  =  S2LG_IN_GA(x1)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x4)
U7_G(x1, x2)  =  U7_G(x1, x2)
U8_G(x1, x2)  =  U8_G(x1, x2)
CONFD_IN_G(x1)  =  CONFD_IN_G(x1)
U2_G(x1, x2)  =  U2_G(x1, x2)
DELA_IN_AGA(x1, x2, x3)  =  DELA_IN_AGA(x2)
U1_AGA(x1, x2, x3, x4, x5)  =  U1_AGA(x3, x5)
U3_G(x1, x2)  =  U3_G(x1, x2)
U4_G(x1, x2)  =  U4_G(x1, x2)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 12 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELA_IN_AGA(X1, .(X2, X3), .(X2, X4)) → DELA_IN_AGA(X1, X3, X4)

The TRS R consists of the following rules:

s2lcG_in_ga(0, []) → s2lcG_out_ga(0, [])
s2lcG_in_ga(s(X1), .(X2, X3)) → U11_ga(X1, X2, X3, s2lcG_in_ga(X1, X3))
U11_ga(X1, X2, X3, s2lcG_out_ga(X1, X3)) → s2lcG_out_ga(s(X1), .(X2, X3))
delcA_in_aga(X1, [], []) → delcA_out_aga(X1, [], [])
delcA_in_aga(X1, .(X1, X2), X2) → delcA_out_aga(X1, .(X1, X2), X2)
delcA_in_aga(X1, .(X2, X3), .(X2, X4)) → U10_aga(X1, X2, X3, X4, delcA_in_aga(X1, X3, X4))
U10_aga(X1, X2, X3, X4, delcA_out_aga(X1, X3, X4)) → delcA_out_aga(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
s2lcG_in_ga(x1, x2)  =  s2lcG_in_ga(x1)
0  =  0
s2lcG_out_ga(x1, x2)  =  s2lcG_out_ga(x1, x2)
U11_ga(x1, x2, x3, x4)  =  U11_ga(x1, x4)
delcA_in_aga(x1, x2, x3)  =  delcA_in_aga(x2)
[]  =  []
delcA_out_aga(x1, x2, x3)  =  delcA_out_aga(x2, x3)
U10_aga(x1, x2, x3, x4, x5)  =  U10_aga(x3, x5)
DELA_IN_AGA(x1, x2, x3)  =  DELA_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELA_IN_AGA(X1, .(X2, X3), .(X2, X4)) → DELA_IN_AGA(X1, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
DELA_IN_AGA(x1, x2, x3)  =  DELA_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELA_IN_AGA(.(X3)) → DELA_IN_AGA(X3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • DELA_IN_AGA(.(X3)) → DELA_IN_AGA(X3)
    The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

S2LG_IN_GA(s(X1), .(X2, X3)) → S2LG_IN_GA(X1, X3)

The TRS R consists of the following rules:

s2lcG_in_ga(0, []) → s2lcG_out_ga(0, [])
s2lcG_in_ga(s(X1), .(X2, X3)) → U11_ga(X1, X2, X3, s2lcG_in_ga(X1, X3))
U11_ga(X1, X2, X3, s2lcG_out_ga(X1, X3)) → s2lcG_out_ga(s(X1), .(X2, X3))
delcA_in_aga(X1, [], []) → delcA_out_aga(X1, [], [])
delcA_in_aga(X1, .(X1, X2), X2) → delcA_out_aga(X1, .(X1, X2), X2)
delcA_in_aga(X1, .(X2, X3), .(X2, X4)) → U10_aga(X1, X2, X3, X4, delcA_in_aga(X1, X3, X4))
U10_aga(X1, X2, X3, X4, delcA_out_aga(X1, X3, X4)) → delcA_out_aga(X1, .(X2, X3), .(X2, X4))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
s2lcG_in_ga(x1, x2)  =  s2lcG_in_ga(x1)
0  =  0
s2lcG_out_ga(x1, x2)  =  s2lcG_out_ga(x1, x2)
U11_ga(x1, x2, x3, x4)  =  U11_ga(x1, x4)
delcA_in_aga(x1, x2, x3)  =  delcA_in_aga(x2)
[]  =  []
delcA_out_aga(x1, x2, x3)  =  delcA_out_aga(x2, x3)
U10_aga(x1, x2, x3, x4, x5)  =  U10_aga(x3, x5)
S2LG_IN_GA(x1, x2)  =  S2LG_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

S2LG_IN_GA(s(X1), .(X2, X3)) → S2LG_IN_GA(X1, X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
S2LG_IN_GA(x1, x2)  =  S2LG_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S2LG_IN_GA(s(X1)) → S2LG_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • S2LG_IN_GA(s(X1)) → S2LG_IN_GA(X1)
    The graph contains the following edges 1 > 1

(22) YES